A:Type, B:(AType), f:fpf(A; x.B(x)), C:Type, a:(A(?C)), b:(CA), y:C.
(y  fpf-domain(compose-fpf(a; b; f)))
 (x:A. ((x  fpf-domain(f))  ((isl(a(x))) c (y = outl(a(x)))))) 

latex

Definitions	t  T, x(s), x. t(x), x:A. B(x), fpf(A; a.B(a)), Unit, b, fpf-domain(f), compose-fpf(a; b; f), P  Q, outl(x), isl(x), prop{i:l}, A c B, (x  l), P  Q, x:A. B(x), P  Q, P  Q, True, T, SqStable(P), if b then t else f fi , , mapfilter(f; P; L)
Lemmas	iff functionality wrt iff, member map filter, mapfilter wf, sq stable from decidable, decidable assert, l member wf, assert wf, isl wf, outl wf, unit wf, fpf wf